abstract sig Bool{}
one sig True extends Bool {}
one sig False extends Bool {}

one abstract sig Email{}

one abstract sig Hash{}

sig Day {}

sig Place {}

enum WeatherType {
	sunny,
	cloudy,
	rainy,
	snow
}

sig Forecast {
	date: one Day,
	place: one Place,
	type: one WeatherType,
	rainlevel: one Int
}

sig Calendar {
	owner: one User,
	events: set Event,
	public: one Bool
}

sig Event {
	date: one Day,
	starttime: one Int,
	endtime: one Int,
	place: one Place,
	creator: one User,
	guests: some User,
	forecast: one Forecast,
	public: one Bool
}

sig User {
	username: one Hash,
	email: one Email,
	badweatherdef: one Int,
	calendar: one Calendar
}

// Facts

// Positive integers
fact intPos {
	{ all i1: Event.starttime | i1 >= 0 }
	{ all i2: Event.endtime | i2 >= 0 }
	{ all i3: Forecast.rainlevel | i3 >= 0 }
}

// Every user has his own calendar
fact userCalendar {
	{ all u: User | u.calendar.owner = u }
	{ all c: Calendar | c = c.owner.calendar }
}

// Events have a positive duration
fact positiveEvents {
	all e: Event | e.starttime < e.endtime
}

// A creator doesn't appear in guests
fact creatorIsntGuest {
	all e: Event | all g: e.guests | g != e.creator
}

// Calendars has only events related to the user owner
fact rightEvents{
	all c: Calendar | all e: c.events | c.owner = e.creator or c.owner in e.guests
}

// Events are added to guests' calendar
fact guestAddEvents {
	all e: Event | all u: e.guests | some e1: u.calendar.events | e1 = e and e1.creator != u
}


// Events are added to creator's calendar
fact ownerAddEvents {
	all e: Event | one e1: e.creator.calendar.events | e1 = e
}

// Events cannot overlap in one's calendar
fact eventCollisionST {
	all c: Calendar | 
	not some e1, e2: c.events | 
	e1!=e2 and e1.date = e2.date 
	and(e1.starttime > e2.starttime and e1.starttime < e2.endtime) 
}
fact eventCollisionET {
	all c: Calendar | 
	not some e1, e2: c.events | 
	e1!=e2 and e1.date = e2.date 
	and(e1.endtime > e2.starttime and e1.endtime < e2.endtime) 
}
fact eventCollisionEQ {
	all c: Calendar | 
	not some e1, e2: c.events | 
	e1!=e2 and e1.date = e2.date 
	and(e1.starttime = e2.starttime or e1.endtime = e2.endtime) 
}

// Forecast for an event is of the same day and place
fact forecastDayPlaceEvent {
	all e: Event | e.date = e.forecast.date and e.place = e.forecast.place
}

// Bad weather definition positive
fact positiveRainlevel {
	all u: User | u.badweatherdef > 0
}

// Rainy days have rainlevel > 0
fact itsRaining {
	all f: Forecast | f.type = rainy => f.rainlevel > 0
}

// Asserts

// An user is either guest or creator of his calendar events
assert userGuestOrCreator {
	all u: User | all e: u.calendar.events | (u in e.guests and u != e.creator) or (u = e.creator and u not in e.guests)
}

check userGuestOrCreator for 5

// If an event has no guests only the creator has it in his calendar
assert partyAlone{
	all c: Calendar | all e: c.events | #(e.guests) = 0 => all u: User | e in u.calendar.events => e.creator = u
}

check partyAlone for 5

// If one has no events in his calendar then he hasn't created events and he's not a guest of any
assert newCalendar {
	all u: User | all e: u.calendar.events | #(u.calendar.events) = 0 <=> (u != e.creator and u not in e.guests)
}

check newCalendar for 15

pred show {}

run show

